w:World, i, x:Id, k:Knd. w-machine-independent(w;i;k;x)  Prop 

latex

Definitions

t  T, Msg(M), x:A. B(x), locl(a), rcv(l,tg), x:AB(x), IdLnk, Id, f(a), x:AB(x), S  T, inr(x), Knd, Unit, Type, left+right, s = t, Prop, True, P  Q, type List, A, P & Q, False, inl(x), outr(x), Void, destination(l), b, b, , a = b, P  Q, tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), w-kindtype(TA;M;i), w-automaton(T;TA;M), w.M, w.T, w.TA, Msg, vartype(i;x), w-machine(w;i), World, w-machine-independent(w;i;k;x)

Lemmas

world wf, Knd wf, w-automaton wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, assert wf, ldst wf, false wf, not wf, Msg wf, IdLnk wf, Id wf, true wf, unit wf, rcv wf, locl wf